Is this what cubicle already does when it creates multiple processes using functory? Or is there something else happening that allows sharing the BFS between multiple processes?

IIUC Unix.fork copies the entire heap onto the new process at the time of creation, but later on the when the process continues the data alterations it makes is local to itself. If that is the case, then this might not be very different from having a per-domain SMT instance and that approach should work on multiple domains, though I'm not sure as yet if the SMT solver itself has any global state that might be affected if we make multiple instances of it. I'll investigate this further and post any updates here.

IIUC Unix.fork copies the entire heap onto the new process at the time of creation, but later on the when the process continues the data alterations it makes is local to itself.

Other than the subtlety that pages are copied-on-write, that is correct. I expect that having the data structures per domain should work.